COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDVAR w w0 w1 w2 ε worlds
C00003 ENDMK
C⊗;
declare INDVAR w w0 w1 w2 ε worlds;
declare INDCONST rw ε worlds;

axiom possible:
	∀m n.(1<m ∧ m<100 ∧ 1<n ∧ n<100 ⊃ ∃w.(M(w) = m ∧ N(w) = n))
	∀w1 w2.(AS0(w1,w2) ∧ AP0(w1,w2))
;;

axiom rw
	M(rw) = m0
	N(rw) = n0
;;

axiom step
	∀w1 w2.((AP1(w1,w2) ≡ AP0(w1,w2) ∧ M(w1)*N(w1) = M(w2)*N(w2))
∧ (AS1(w1,w2) ≡ AS0(w1,w2) ∧ M(w1)+N(w1) = M(w2)+N(w2)))
;;